Problem:
 0(1(2(3(4(x1))))) -> 0(2(1(3(4(x1)))))
 0(5(1(2(4(3(x1)))))) -> 0(5(2(1(4(3(x1))))))
 0(5(2(4(1(3(x1)))))) -> 0(1(5(2(4(3(x1))))))
 0(5(3(1(2(4(x1)))))) -> 0(1(5(3(2(4(x1))))))
 0(5(4(1(3(2(x1)))))) -> 0(5(4(3(1(2(x1))))))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {6}
   transitions:
    01(11) -> 12*
    51(45) -> 46*
    51(64) -> 65*
    41(80) -> 81*
    41(42) -> 43*
    41(7) -> 8*
    41(29) -> 30*
    41(31) -> 32*
    41(21) -> 22*
    41(23) -> 24*
    31(75) -> 76*
    31(55) -> 56*
    31(47) -> 48*
    31(79) -> 80*
    31(61) -> 62*
    31(41) -> 42*
    31(53) -> 54*
    31(8) -> 9*
    11(65) -> 66*
    11(9) -> 10*
    11(78) -> 79*
    11(43) -> 44*
    21(10) -> 11*
    21(97) -> 98*
    21(77) -> 78*
    21(99) -> 100*
    21(89) -> 90*
    21(74) -> 75*
    21(44) -> 45*
    21(91) -> 92*
    21(63) -> 64*
    00(5) -> 6*
    00(2) -> 6*
    00(4) -> 6*
    00(1) -> 6*
    00(3) -> 6*
    10(5) -> 1*
    10(2) -> 1*
    10(4) -> 1*
    10(1) -> 1*
    10(3) -> 1*
    20(5) -> 2*
    20(2) -> 2*
    20(4) -> 2*
    20(1) -> 2*
    20(3) -> 2*
    30(5) -> 3*
    30(2) -> 3*
    30(4) -> 3*
    30(1) -> 3*
    30(3) -> 3*
    40(5) -> 4*
    40(2) -> 4*
    40(4) -> 4*
    40(1) -> 4*
    40(3) -> 4*
    50(5) -> 5*
    50(2) -> 5*
    50(4) -> 5*
    50(1) -> 5*
    50(3) -> 5*
    1 -> 97,55,29
    2 -> 89,47,21
    3 -> 99,61,31
    4 -> 91,53,23
    5 -> 77,41,7
    8 -> 74*
    12 -> 6*
    22 -> 8*
    24 -> 8*
    30 -> 8*
    32 -> 8*
    43 -> 63*
    46 -> 11*
    48 -> 42*
    54 -> 42*
    56 -> 42*
    62 -> 42*
    66 -> 11*
    76 -> 64*
    81 -> 45*
    90 -> 78*
    92 -> 78*
    98 -> 78*
    100 -> 78*
  problem:
   
  Qed